%--
\chapter{引言}

分布式系统的基础知识。

\myleaf 分布式系统的经典教科书 \cite{Tanenbaum06}。\\

形式化验证的基础知识

\myleaf 数理逻辑与软件形式化验证基础知识 \cite{Huth04}。\\

TLA+

\myleaf TLA+的基础知识 \footnote{Leslie Lamport, The TLA+ Home Page: http://lamport.azurewebsites.net/tla/tla.html}。

\myleaf TLA+教程 \cite{Wayne18}。\\

分布式系统的形式化验证的工业界实践。

\myleaf Amazon的实践 \cite{Newcombe15}。\\

面向教学的分布式算法快速实现。

\myleaf DSLabs \cite{Michael19}。

%--
\chapter{分布式计算模型}

%--------------------------------------------------------------------------------
\section{系统建模}

%----------------------------------------
\subsection{计算模型的基本概念 --- 一个二维框架}

首先了解计算模型的基本概念。可以从两个维度来了解计算模型的基本构成。一个维度是时间，相应的有同步模型和异步模型。一个维度是(空间)通信方式，包括消息传递(简称为MSG)模型和共享存储(简称为SHM)模型。

\myleaf 阅读\cite{Attiya04}的第1、2、4章。阅读\cite{Aspnes19}的第2、15章。

\myleaf 计算模型的二维构成，参加L1胶片中的图。

%----------------------------------------
\subsection{模型间模拟的概念}

其次要了解计算模型之间的模拟(simulation)这一引申概念。了解模拟本身之外，还需要辨析、深入理解不同计算模型的优劣、权衡。

\myleaf 阅读\cite{Attiya04}的第7、9章。阅读\cite{Aspnes19}的第16章。

%----------------------------------------
\subsection{失效模型的基本概念}

首先了解crash failure、Byzantine failure、link failure的基本定义和大致含义，后面结合具体的问题、算法、系统，做进一步了解。


%--------------------------------------------------------------------------------
\section{特定领域分布式系统的建模}

%----------------------------------------
\subsection{分布式数据库系统}

数据划分(partition, sharding)的问题。

数据复制(replication)的问题。

对上层应用编程提供事务(transaction)的支持。

分布式数据库中的容错问题。


%----------------------------------------
\subsection{分布式消息分发中间件}

分布式消息分发系统，分布式消息中间件(DMS, Distributed Messaging System)。

发布-订阅(Pub-Sub, Publish-Subscribe)系统。




%--------------------------------------------------------------------------------
\section{问题规约}

问题的规约(specification)。

安全性(safety)。

活性(liveness)。

%----------------------------------------
\subsection{问题间的归约}

问题之间的归约(reduction)。


%--------------------------------------------------------------------------------
\section{消息传递模型}

%----------------------------------------
\subsection{同步}

%----------------------------------------
\subsection{异步}


%--------------------------------------------------------------------------------
\section{共享内存模型}









